The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

eq(0, 0) → true [1]
eq(0, s(X)) → false [1]
eq(s(X), 0) → false [1]
eq(s(X), s(Y)) → eq(X, Y) [1]
rm(N, nil) → nil [1]
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X)) [1]
ifrm(true, N, add(M, X)) → rm(N, X) [1]
ifrm(false, N, add(M, X)) → add(M, rm(N, X)) [1]
purge(nil) → nil [1]
purge(add(N, X)) → add(N, purge(rm(N, X))) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

eq(0, 0) → true [1]
eq(0, s(X)) → false [1]
eq(s(X), 0) → false [1]
eq(s(X), s(Y)) → eq(X, Y) [1]
rm(N, nil) → nil [1]
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X)) [1]
ifrm(true, N, add(M, X)) → rm(N, X) [1]
ifrm(false, N, add(M, X)) → add(M, rm(N, X)) [1]
purge(nil) → nil [1]
purge(add(N, X)) → add(N, purge(rm(N, X))) [1]

The TRS has the following type information:

eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false rm :: 0:s → nil:add → nil:add nil :: nil:add add :: 0:s → nil:add → nil:add ifrm :: true:false → 0:s → nil:add → nil:add purge :: nil:add → nil:add

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

purge

(c) The following functions are completely defined:

eq
rm
ifrm

Due to the following rules being added:

ifrm(v0, v1, v2) → nil [0]

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) → true [1] eq(0, s(X)) → false [1] eq(s(X), 0) → false [1] eq(s(X), s(Y)) → eq(X, Y) [1] rm(N, nil) → nil [1] rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X)) [1] ifrm(true, N, add(M, X)) → rm(N, X) [1] ifrm(false, N, add(M, X)) → add(M, rm(N, X)) [1] purge(nil) → nil [1] purge(add(N, X)) → add(N, purge(rm(N, X))) [1] ifrm(v0, v1, v2) → nil [0] The TRS has the following type information: eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false rm :: 0:s → nil:add → nil:add nil :: nil:add add :: 0:s → nil:add → nil:add ifrm :: true:false → 0:s → nil:add → nil:add purge :: nil:add → nil:add Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) → true [1] eq(0, s(X)) → false [1] eq(s(X), 0) → false [1] eq(s(X), s(Y)) → eq(X, Y) [1] rm(N, nil) → nil [1] rm(0, add(0, X)) → ifrm(true, 0, add(0, X)) [2] rm(0, add(s(X'), X)) → ifrm(false, 0, add(s(X'), X)) [2] rm(s(X''), add(0, X)) → ifrm(false, s(X''), add(0, X)) [2] rm(s(X1), add(s(Y'), X)) → ifrm(eq(X1, Y'), s(X1), add(s(Y'), X)) [2] ifrm(true, N, add(M, X)) → rm(N, X) [1] ifrm(false, N, add(M, X)) → add(M, rm(N, X)) [1] purge(nil) → nil [1] purge(add(N, nil)) → add(N, purge(nil)) [2] purge(add(N, add(M', X2))) → add(N, purge(ifrm(eq(N, M'), N, add(M', X2)))) [2] ifrm(v0, v1, v2) → nil [0] The TRS has the following type information: eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false rm :: 0:s → nil:add → nil:add nil :: nil:add add :: 0:s → nil:add → nil:add ifrm :: true:false → 0:s → nil:add → nil:add purge :: nil:add → nil:add Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
true => 1
false => 0
nil => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' = 1 + X, X >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z = 1 + X, X >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(N, X) :|: z'' = 1 + M + X, z = 1, X >= 0, z' = N, M >= 0, N >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(N, X) :|: z'' = 1 + M + X, X >= 0, z' = N, z = 0, M >= 0, N >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 2 }→ 1 + N + purge(ifrm(eq(N, M'), N, 1 + M' + X2)) :|: M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + N + purge(0) :|: z = 1 + N + 0, N >= 0
rm(z, z') -{ 2 }→ ifrm(eq(X1, Y'), 1 + X1, 1 + (1 + Y') + X) :|: X1 >= 0, Y' >= 0, z = 1 + X1, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + X) :|: z' = 1 + 0 + X, X >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + X'', 1 + 0 + X) :|: z = 1 + X'', z' = 1 + 0 + X, X >= 0, X'' >= 0
rm(z, z') -{ 1 }→ 0 :|: z = N, z' = 0, N >= 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 2 }→ 1 + N + purge(ifrm(eq(N, M'), N, 1 + M' + X2)) :|: M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 2 }→ ifrm(eq(z - 1, Y'), 1 + (z - 1), 1 + (1 + Y') + X) :|: z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ eq } { ifrm, rm } { purge }

(14) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 2 }→ 1 + N + purge(ifrm(eq(N, M'), N, 1 + M' + X2)) :|: M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 2 }→ ifrm(eq(z - 1, Y'), 1 + (z - 1), 1 + (1 + Y') + X) :|: z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {eq}, {ifrm,rm}, {purge}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: eq
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(16) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 2 }→ 1 + N + purge(ifrm(eq(N, M'), N, 1 + M' + X2)) :|: M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 2 }→ ifrm(eq(z - 1, Y'), 1 + (z - 1), 1 + (1 + Y') + X) :|: z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {eq}, {ifrm,rm}, {purge}
Previous analysis results are:

eq: runtime: ?, size: O(1) [1]

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: eq
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(18) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 2 }→ 1 + N + purge(ifrm(eq(N, M'), N, 1 + M' + X2)) :|: M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 2 }→ ifrm(eq(z - 1, Y'), 1 + (z - 1), 1 + (1 + Y') + X) :|: z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {ifrm,rm}, {purge}
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1]

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 3 + M' }→ 1 + N + purge(ifrm(s'', N, 1 + M' + X2)) :|: s'' >= 0, s'' <= 1, M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 3 + Y' }→ ifrm(s', 1 + (z - 1), 1 + (1 + Y') + X) :|: s' >= 0, s' <= 1, z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {ifrm,rm}, {purge}
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: ifrm
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z''

Computed SIZE bound using KoAT for: rm
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(22) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 3 + M' }→ 1 + N + purge(ifrm(s'', N, 1 + M' + X2)) :|: s'' >= 0, s'' <= 1, M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 3 + Y' }→ ifrm(s', 1 + (z - 1), 1 + (1 + Y') + X) :|: s' >= 0, s' <= 1, z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {ifrm,rm}, {purge}
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1] ifrm: runtime: ?, size: O(n1) [z''] rm: runtime: ?, size: O(n1) [z']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: ifrm
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 22·z'' + 2·z''²

Computed RUNTIME bound using KoAT for: rm
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 118 + 165·z' + 20·z'²

(24) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 1 }→ rm(z', X) :|: z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 1 }→ 1 + M + rm(z', X) :|: z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 3 + M' }→ 1 + N + purge(ifrm(s'', N, 1 + M' + X2)) :|: s'' >= 0, s'' <= 1, M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 3 + Y' }→ ifrm(s', 1 + (z - 1), 1 + (1 + Y') + X) :|: s' >= 0, s' <= 1, z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 2 }→ ifrm(1, 0, 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 0, 1 + (1 + X') + X) :|: X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 2 }→ ifrm(0, 1 + (z - 1), 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {purge}
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1] ifrm: runtime: O(n2) [1 + 22·z'' + 2·z''2], size: O(n1) [z''] rm: runtime: O(n2) [118 + 165·z' + 20·z'2], size: O(n1) [z']

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 119 + 165·X + 20·X² }→ s5 :|: s5 >= 0, s5 <= 1 * X, z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 119 + 165·X + 20·X² }→ 1 + M + s6 :|: s6 >= 0, s6 <= 1 * X, z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 28 + 27·M' + 4·M'·X2 + 2·M'² + 26·X2 + 2·X2² }→ 1 + N + purge(s7) :|: s7 >= 0, s7 <= 1 * (1 + M' + X2), s'' >= 0, s'' <= 1, M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 3 + 22·z' + 2·z'² }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + 0 + (z' - 1)), z' - 1 >= 0, z = 0
rm(z, z') -{ 55 + 30·X + 4·X·X' + 2·X² + 30·X' + 2·X'² }→ s2 :|: s2 >= 0, s2 <= 1 * (1 + (1 + X') + X), X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 3 + 22·z' + 2·z'² }→ s3 :|: s3 >= 0, s3 <= 1 * (1 + 0 + (z' - 1)), z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 56 + 30·X + 4·X·Y' + 2·X² + 31·Y' + 2·Y'² }→ s4 :|: s4 >= 0, s4 <= 1 * (1 + (1 + Y') + X), s' >= 0, s' <= 1, z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {purge}
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1] ifrm: runtime: O(n2) [1 + 22·z'' + 2·z''2], size: O(n1) [z''] rm: runtime: O(n2) [118 + 165·z' + 20·z'2], size: O(n1) [z']

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: purge
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(28) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 119 + 165·X + 20·X² }→ s5 :|: s5 >= 0, s5 <= 1 * X, z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 119 + 165·X + 20·X² }→ 1 + M + s6 :|: s6 >= 0, s6 <= 1 * X, z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 28 + 27·M' + 4·M'·X2 + 2·M'² + 26·X2 + 2·X2² }→ 1 + N + purge(s7) :|: s7 >= 0, s7 <= 1 * (1 + M' + X2), s'' >= 0, s'' <= 1, M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 3 + 22·z' + 2·z'² }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + 0 + (z' - 1)), z' - 1 >= 0, z = 0
rm(z, z') -{ 55 + 30·X + 4·X·X' + 2·X² + 30·X' + 2·X'² }→ s2 :|: s2 >= 0, s2 <= 1 * (1 + (1 + X') + X), X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 3 + 22·z' + 2·z'² }→ s3 :|: s3 >= 0, s3 <= 1 * (1 + 0 + (z' - 1)), z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 56 + 30·X + 4·X·Y' + 2·X² + 31·Y' + 2·Y'² }→ s4 :|: s4 >= 0, s4 <= 1 * (1 + (1 + Y') + X), s' >= 0, s' <= 1, z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed: {purge}
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1] ifrm: runtime: O(n2) [1 + 22·z'' + 2·z''2], size: O(n1) [z''] rm: runtime: O(n2) [118 + 165·z' + 20·z'2], size: O(n1) [z'] purge: runtime: ?, size: O(n1) [z]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: purge
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 1 + 30·z + 53·z² + 8·z³

(30) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifrm(z, z', z'') -{ 119 + 165·X + 20·X² }→ s5 :|: s5 >= 0, s5 <= 1 * X, z'' = 1 + M + X, z = 1, X >= 0, M >= 0, z' >= 0
ifrm(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
ifrm(z, z', z'') -{ 119 + 165·X + 20·X² }→ 1 + M + s6 :|: s6 >= 0, s6 <= 1 * X, z'' = 1 + M + X, X >= 0, z = 0, M >= 0, z' >= 0
purge(z) -{ 1 }→ 0 :|: z = 0
purge(z) -{ 28 + 27·M' + 4·M'·X2 + 2·M'² + 26·X2 + 2·X2² }→ 1 + N + purge(s7) :|: s7 >= 0, s7 <= 1 * (1 + M' + X2), s'' >= 0, s'' <= 1, M' >= 0, X2 >= 0, z = 1 + N + (1 + M' + X2), N >= 0
purge(z) -{ 2 }→ 1 + (z - 1) + purge(0) :|: z - 1 >= 0
rm(z, z') -{ 3 + 22·z' + 2·z'² }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + 0 + (z' - 1)), z' - 1 >= 0, z = 0
rm(z, z') -{ 55 + 30·X + 4·X·X' + 2·X² + 30·X' + 2·X'² }→ s2 :|: s2 >= 0, s2 <= 1 * (1 + (1 + X') + X), X >= 0, X' >= 0, z' = 1 + (1 + X') + X, z = 0
rm(z, z') -{ 3 + 22·z' + 2·z'² }→ s3 :|: s3 >= 0, s3 <= 1 * (1 + 0 + (z' - 1)), z' - 1 >= 0, z - 1 >= 0
rm(z, z') -{ 56 + 30·X + 4·X·Y' + 2·X² + 31·Y' + 2·Y'² }→ s4 :|: s4 >= 0, s4 <= 1 * (1 + (1 + Y') + X), s' >= 0, s' <= 1, z - 1 >= 0, Y' >= 0, X >= 0, z' = 1 + (1 + Y') + X
rm(z, z') -{ 1 }→ 0 :|: z' = 0, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

eq: runtime: O(n1) [1 + z'], size: O(1) [1] ifrm: runtime: O(n2) [1 + 22·z'' + 2·z''2], size: O(n1) [z''] rm: runtime: O(n2) [118 + 165·z' + 20·z'2], size: O(n1) [z'] purge: runtime: O(n3) [1 + 30·z + 53·z2 + 8·z3], size: O(n1) [z]

(31) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(32) BOUNDS(1, n^3)